(declare-fun a () String)
(declare-fun z () String)
(declare-fun c () String)
(declare-fun aa () String)
(declare-fun d () Bool)
(declare-fun e () Bool)
(declare-fun b () Bool)
(declare-fun f () Bool)
(declare-fun GohuV_new () Bool)
(declare-fun g () Bool)
(declare-fun h () Bool)
(declare-fun i () Bool)
(declare-fun ac () String)
(declare-fun j () Int)
(declare-fun k () String)
(declare-fun m () String)
(declare-fun n () String)
(declare-fun l () String)
(declare-fun p () Bool)
(declare-fun s () Bool)
(declare-fun o () Bool)
(declare-fun t () Bool)
(declare-fun q () Bool)
(declare-fun r () Bool)
(declare-fun u () String)
(declare-fun v () Bool)
(declare-fun w () Bool)
(declare-fun af () String)
(assert (= (= d (not (= e s))) (= "" (str.substr ac 21 (str.len u)))))
(assert (= (= "-" (str.substr ac 25 (str.len u))) o s))
(assert (= f (and (= GohuV_new q))))
(assert (= (not (= j 43)) (or (= (str.substr z 21 (str.len m)) "__utma=16886264.") (or (str.in.re (str.substr c 30 (str.len n)) (re.++ (str.to.re "") (re.++ (str.to.re "") (re.++ (str.to.re "") (re.++ (str.to.re "t") (re.++ (str.to.re "") (re.++ (str.to.re "a") (re.++ (str.to.re "=") (re.++ (str.to.re "1") (re.++ (str.to.re "6") (re.++ (str.to.re "8") (re.++ (str.to.re "8") (re.++ (str.to.re "6") (re.++ (str.to.re "2") (re.++ (str.to.re "") (re.++ (str.to.re "") (str.to.re "."))))))))))))))))))) (or (= j 0) (= g (not (= h r)))) (= "" (str.substr ac 0 (str.len u))) (or (= h v))))
(assert (not (= i v)))
(assert (= (or f t) (not (= d p)) (and (= "" (str.substr a (str.len k) (str.len (str.substr z (str.len m) (str.len (str.substr aa (str.len l) (str.len (str.substr ac (str.len u) (str.len af))))))))))))
(assert (not (= b o)))
(assert (= a (str.++ k af) z (str.++ m af)))
(assert (= c aa (str.++ l af)))
(assert (= d (not (= p w))))
(assert (= e (or (= s w)) b f (and (= r v))))
(check-sat)
